w:World. FairFifo  (e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id)) 

latex

Definitions	World, t  T, x:AB(x), FairFifo, E, <a, b>, w-pred(w;e), x.A(x), pred(e), loc(e), Id, s = t, first(e), b, A, P  Q, x:A. B(x), , False, b, , , #$n, A  B, n - m, -n, n+m, a < b, Void, {x:A| B(x)} , , a(i;t), isnull(a), x:A  B(x), P & Q, P  Q, Unit, left + right, True, ff, (i = j), time(e), i  j , Type, isl(x), P  Q, loc(e)
Lemmas	first wf, fair-fifo wf, w-loc-lemma, pred wf, w-pred wf, w-pred-wf2, isl wf, w-E wf, unit wf, ge wf, nat properties, nat wf, Id wf, not functionality wrt iff, assert of eq int, eq int wf, true wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, w-isnull wf, w-a wf, le wf, bool wf, bnot wf, assert wf, not wf, false wf, world wf